% !Mode:: "TeX:UTF-8"
\documentclass[14pt,autoref,href
%,fixint=false
,facsimile=false
]{disser}

\usepackage{cmap}
\usepackage[a4paper, nohead, includefoot, mag=1000,
            margin=2cm, top=1.5cm, bottom=1.5cm, footskip=1cm]{geometry}
%\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenx}
\usepackage[english,russian]{babel}
\usepackage{tabularx}
%\usepackage{epstopdf}
\usepackage{amsthm}
\usepackage{xspace}
\usepackage{ifthen}


\renewcommand{\baselinestretch}{1.4}

% Поддержка нескольких списков литературы в одном документе
%\usepackage{multibib}
% Создание команд для цитирования собственных работ диссертанта
% в отдельном разделе. В данном случае ссылка будет иметь вид \citemy{...}.
%\newcites{my}{Список публикаций}

\newtheorem{utv}{Утверждение}
\newtheorem{theorem}{Теорема}
\newtheorem{assumption}{Предположение}
%\newtheorem{heuristics}{Эвристика}
\newtheorem{definition}{Определение}{\bfseries}{\itshape}
%% Путь к файлам с иллюстрациями
%\graphicspath{{fig/}}

% Теперь "русифицируем" окружение enumerate:
\makeatletter
\def\labelenumi{\theenumi)}      % чтобы после номера шла скобка;
\def\theenumii{\@asbuk\c@enumii}   % чтобы на втором уровне шли русские,
\def\labelenumii{\theenumii)}    % а не латинские буквы
\def\p@enumii{\theenumi}         % а это для \ref
\def\labelenumiii{{\bf--}}       % а на третьем уровне пусть будут лишь тире,
\let\theenumiii\relax            % и отдельных ссылок на него не будет
\def\p@enumiii{\theenumi\theenumii}
\makeatother

\usepackage{ifpdf}

\ifpdf
% we are running pdflatex, so convert .eps files to .pdf
% run pdflatex with --shell-escape and thesis.aux
\usepackage[pdftex]{graphicx}
\usepackage{epstopdf}
\else
% we are running LaTeX, not pdflatex
\usepackage{graphicx}
\fi

% Включение файла с общим текстом диссертации и автореферата
% (текст титульного листа и характеристика работы).
\input{common}

\include{../phi/theorems}%eps/theorems}
\include{../phi/intro11}%eps/intro11}

\newcommand{\LRU}{LRU\xspace}
\newcommand{\FIFO}{FIFO\xspace}
\newcommand{\PseudoLRU}{Pseudo-LRU\xspace}

\renewcommand{\facsimile}{\vspace{0.5cm}\includegraphics[width=3cm]{my}}
% --------------------------------------------------------------------------
\begin{document}

% Внешняя сторона обложки
\title{АВТОРЕФЕРАТ\\
диссертации на соискание ученой степени\\
кандидата физико-математических наук}

\maketitle

% Внутренняя сторона обложки
\noindent
Работа выполнена на кафедре системного программирования факультета вычислительной математики и кибернетики Московского государственного университета имени М. В. Ломоносова.
\vskip1ex
\noindent\begin{tabularx}{\linewidth}{lp{0.3cm}X}
Научный руководитель:  & & \emph{доктор физико-математических наук,} \\
                       & & \emph{старший научный сотрудник} \\
                       & & \emph{\textbf{Петренко Александр Константинович}}.
\\
Официальные оппоненты: & & \emph{доктор физико-математических наук}, \\
                       & & \emph{профессор} \\
                       & & \emph{\textbf{Смелянский Руслан Леонидович}};\\
                       & & \emph{доктор физико-математических наук} \\
                       & & \emph{\textbf{Лацис Алексей Оттович}}.
\\
Ведущая организация:   & & \emph{Научно-исследовательский институт}\\
& & \emph{системных исследований РАН}
\end{tabularx}

\vskip2ex\noindent
Защита состоится %<<\underline{15}>> \underline{октября} 2010 года в \underline{11} часов
26 ноября 2010 года в 11 часов
на заседании диссертационного совета \emph{Д 501.001.44} \emph{Московского
государственного университета имени М.В. Ломоносова} по адресу:
\emph{119991, ГСП-1, Москва, Ленинские горы, МГУ имени М.В.Ломоносова, 2-й учебный корпус, факультет ВМК, ауд. 685.}

\vskip1ex\noindent
С диссертацией можно ознакомиться в библиотеке
\emph{факультета ВМК МГУ}.
С текстом автореферата можно ознакомиться на официальном сайте ВМК МГУ \underline{http://cs.msu.ru} в разделе <<Наука>> --- <<Работа диссертационных советов>> --- <<Д 501.001.44>>

\vskip1ex\noindent
Автореферат разослан <<14>> сентября 2010 г.
%\vskip2ex\noindent
%Отзывы и замечания по автореферату в двух экземплярах, заверенные печатью, просьба высылать по вышеуказанному адресу на имя ученого секретаря диссертационного совета.

\vfill\noindent
\raisebox{-30pt}[1pt][10pt]{\includegraphics[width=1cm]{sh}}
Ученый секретарь

\hspace{0.4cm}диссертационного совета

\hspace{0.4cm}\emph{профессор}%
%
%\makeatletter
% вставка файла, содержащего факсимиле ученого секретаря
%\ifDis@facsimile
  %\raisebox{100pt}{\includegraphics[width=4cm]{korolev}}\hfill
  \hspace{5cm}\raisebox{-4pt}[1pt][10pt]{\includegraphics[width=4cm]{korolev}}
%\fi%
%\makeatother%
%
\hfill
\emph{Н.П. Трифонов}

\clearpage

\section*{Общая характеристика работы}

\subsection*{Актуальность темы}
\newcommand{\nocites}{}
\Actuality

\subsection*{Цель диссертационной работы}
\Objective

\subsection*{Научная новизна}
\Novelty

\subsection*{Практическая значимость}
\PracticalValue

% Результаты и положения, выносимые на защиту
%\resultssection
%\resultstext

% Апробация работы
%\approbationsection
%\approbationtext

\subsection*{Апробация работы и публикации}
\Pub

% Личный вклад автора
%\contribsection
%\contribtext

\subsection*{Структура и объем диссертации}
\Structure


%
% -----------------------------------------------------------------------
%


\section*{Содержание работы}

\paragraph{Во Введении} обоснована актуальность диссертационной работы,
сформулирована цель и задачи исследований, сформулированы полученные результаты и показана их
практическая значимость.

%
% -----------------------------------------------------------------------
%


\paragraph{Первая глава} содержит обзор существующих методов построения тестовых программ, обзор подсистем управления памяти и уточнение задач исследования по результатам этих обзоров.

В разделе 1.1 дается схема системного тестирования микропроцессора, описываются его отдельные этапы, в том числе и этап построения тестовых программ. Рассматриваются методы псевдослучайного и целенаправленного автоматического построения тестовых программ. В разделе 1.2 кратко описываются функции и типичный состав подсистем управления памяти, способы повышения их эффективности и классы ошибок. В разделе 1.3 сделан обзор методов целенаправленного построения тестовых программ. Выделены методы на основе массовой генерации тестовых программ и методы непосредственного построения тестовых программ. В разделе 1.4 сделан анализ методов целенаправленного построения тестовых программ по применимости этих методов для тестирования подсистем управления памяти, масштабируемости, возможности <<нацеливания>> на функциональность. Наиболее перспективными являются методы непосредственного построения тестовых программ по тестовым ситуациям, формализованным в виде \emph{тестовых шаблонов} --- цепочек инструкций с указанием вариантов исполнения инструкций --- и методы, включающие разрешение ограничений (constraint satisfaction). В разделе 1.5 уточнены задачи в соответствии с проведенным исследованием методов построения тестовых программ.

\paragraph{Во второй главе} предложен подход целенаправленного построения нацеленных тестовых программ, сочетающий особенности перспективных методов построения тестовых программ. В разделе 2.1 описаны этапы построения тестовых программ согласно предлагаемому подходу: чтение документации по архитектуре, формализация архитектуры, выделение и формализация тестовых ситуаций (в виде шаблонов тестовых программ, далее \emph{тестовых шаблонов}), построение и решение системы ограничений для каждого тестового шаблона, конструирование текста тестовой программы на основе решения каждой совместной системы ограничений.

Тестовый шаблон содержит последовательность инструкций, для каждой из которых указан вариант исполнения (т.е. некоторый путь выполнения инструкции). Для алгоритмического построения ограничений и затем тестовых программ варианта инструкций должны быть формализованы в рамках этапа формализации микропроцессора. Раздел 2.2 более детально освещает этот этап . В этом разделе предложены модель функционирования устройств подсистемы управления памяти и модель вариантов инструкций. В рамках этого этапа следует выделить и формализовать те варианты инструкций, которые входят в тестовый шаблон, и задействованные в них устройства подсистемы управления памяти. Моделью состояния устройства подсистемы управления памяти (кэш-памяти, таблицы страниц и т.п.) предлагается последовательность ассоциативных массивов (далее эта последовательность будет называться \emph{таблицей}, а отдельный ассоциативный массив --- \emph{регионом}). Каждый регион состоит из \emph{строк}, каждая строка состоит из набора \emph{полей}, поля делятся на \emph{поля ключа} и \emph{поля данных}. Поля ключа задают ключи в ассоциативном массиве, поля данных --- значения. В модели устройства определены следующие операции: успешного обращения, успешного обращения с изменением, неуспешного обращения с замещением. На входе операции успешного обращения --- выражение, задающие ключ, и выражение, задающее номер ассоциативного массива из состояния устройства. Операция определена на тех входных данных и состоянии модели, при которых в соответствующем ассоциативном массиве есть строка, поля ключей которой \emph{соответствуют} аргументу-ключу этой операции. Операция возвращает поля данных соответствующей аргументу-ключу строки. Операция успешного обращения с изменением отличается от операции успешного обращения дополнительным аргументом --- полями данных, которые нужно заменить в строке, соответствующей аргументу-ключу. На входе операции  неуспешного обращения с замещением 3 аргумента: выражение, задающие ключ, выражение, задающее номер ассоциативного массива, и выражения для полей данных строки. Операция определена на тех входных данных и состоянии модели, при которых в соответствующем ассоциативном массиве нет строки, поля ключей которой \emph{соответствуют} аргументу-ключу этой операции. Эффект операции заключается в замене полей данных одной из строк в ассоциативном массиве, номер которого был передан в качестве одного из аргументов операции, на переданные операции поля данных. Выбор строки для замены определяется на основе стратегии вытеснения так же, как это делается в устройствах подсистемы управления памяти (например, в кэш-памяти). В рамках этапа формализации следует указать набор атрибутов, задающих модели устройств тестируемой подсистемы управления памяти: стратегия вытеснения, количество строк в массиве (<<ассоциативность>>), двоичный логарифм количества массивов, имена и битовые длины полей ключа и полей данных, предикат соответствия строки некоторой битовой строке (эта строка является аргументом-ключом в операциях над моделью). Алгоритмы построения систем ограничений параметризованы этими атрибутами. Таким образом моделируются кэш-память различных уровней, таблицы страниц, буферы трансляции адресов (TLB) и даже оперативная память.

В том же разделе предложены модели вариантов инструкций. Варианты инструкций соответствуют отдельным путям выполнения инструкций. Модель варианта инструкции формализует следующие виды требований: допустимые значения операндов инструкции, вычисление значений операндов-результатов инструкции, условия возникновения исключительных ситуаций (если вариант инструкции состоит в возникновении такой ситуации), вычисление адресов (физических, виртуальных, эффективных) в инструкции, обращения в устройства подсистемы управления памяти и успешность этих обращений, какие данные загружаются или сохраняются. При формализации для варианта инструкции объявляются операнды инструкции и последовательность операторов 4-х видов: оператор утверждения истинности свойства над битовыми строками (\texttt{assume}), оператор введения новой переменной (\texttt{let}), оператор попадания (\texttt{hit}), оператор промаха (\texttt{miss}). С помощью этой последовательности операторов задается набор условий на значения операндов инструкции и для моделей устройств, задействованных в этом варианте инструкции, условия на их состояние и изменение этого состояния в рамках данного варианта. Операторы \texttt{let} и \texttt{assume} имеют ту же семантику, которая используется при формализации императивных языков программирования. Операторы \texttt{hit} и \texttt{miss} специфичны инструкциям, оперирующим с памятью. Оператор попадания \texttt{hit<B>(k;R)\{loaded(d); [storing(d');] \}}, где \texttt{k, R, d, d'} --- выражения над определенными ранее переменными-битовыми строками, означает, что в данном варианте инструкции должно осуществляться успешное обращение в устройство \texttt{B} по ключу \texttt{k} в массив с номером \texttt{R}, причем ключу соответствуют данные \texttt{d} (если полей данных несколько, то соответствующие выражения для них перечисляются в скобках у \texttt{loaded}). Если указана секция \texttt{storing}, то в варианте инструкции должно осуществляться успешное обращение с изменением на поля данных \texttt{d'}. Оператор промаха \texttt{miss<B>(k;R)\{[replacing(d);]\}}, где \texttt{k, R, d} --- выражения над определенными ранее переменными-битовыми строками, означает, что в данном варианте инструкции должно быть неуспешное обращение в устройство \texttt{B} по ключу \texttt{k} в массив с номером \texttt{R}. Секция \texttt{replacing} задает поля данных \texttt{d'} вытесняющей строки. Если секция \texttt{replacing} отсутствует, изменение состояния устройства \texttt{B} не должно происходить.

Формализовав устройства подсистемы управления памяти и инструкции и составив тестовый шаблон, нужно определить те значения регистров и хранящиеся данные устройств, при которых исполнение инструкций, указанных в тестовом шаблоне, будет проходить согласно указанным там вариантам. Для этого составляется система ограничений, выражающая все необходимые условия на такие значения. В результате разрешения этой системы определяются искомые значения. В разделе 2.3 описывается предлагаемый алгоритм построения ограничений для тестового шаблона. Исполнение инструкций конвейеризовано, поэтому расположенные рядом инструкции в действительности будут выполняться с существенной долей параллелизма. Однако в алгоритме генерации ограничений считается, что инструкции выполняются последовательно, а тестовые шаблоны составлены таким образом, чтобы при работе соответствующих им тестовых программ проявились все нужные параллельные эффекты.

По каждому оператору алгоритм строит свою часть ограничений, которые выражают семантику этого оператора. Операторы обращений в устройства транслируются в ограничения без моделирования состояний устройств, несмотря на то, что определение этих операторов включало состояние устройства. Это позволяет существенно уменьшить количество переменных-битовых строк и размер ограничений и, тем самым, ускорить разрешение ограничений. Специальное представление выбрано и для начального содержимого устройств, а именно, последовательность обращений в это устройство. Поэтому в число переменных в ограничениях входят переменные, задающие аргументы этих, \emph{инициализирующих}, обращений: ключи, номера ассоциативных массивов. Для операторов \texttt{hit} и \texttt{miss} строятся ограничения на аргументы-ключи \texttt{k} и номера регионов \texttt{R} (эти ограничения должны гарантировать успешное обращение для \texttt{hit} и неуспешное --- для \texttt{miss}) и ограничения на аргументы-данные \texttt{d} и \texttt{d'} (обращения по одинаковым адресам должны давать одинаковые данные, если они не были изменены). Ограничения на аргументы-ключи и аргументы-номера регионов строятся согласно следующим определениям операторов: \texttt{hit(k$_i$;R$_i$)} / \texttt{miss(k$_i$;R$_i$)} происходит, если
\begin{itemize}
\item[$(\alpha)$] перед ним есть обращение по тому же ключу (\texttt{k}$_i$) в тот же регион (\texttt{R}$_i$),
\item[$(\beta)$] после которого и до этого обращения соответствующая строка \underline{не была} \underline{вытеснена} / \underline{была вытеснена} из таблицы.
\end{itemize}

Трансляция свойства $\alpha$ достаточно очевидна, трансляция свойства $\beta$ рассматривается в разделе 2.5.

В этом же разделе диссертации сформулированы и доказаны теоремы корректности и полноты алгоритмов, гарантирующие, что ограничений, построенные согласно алгоритму, не дают решений, не соответствующих тестовому шаблону, и задают все решения, соответствующие тестовому шаблону. Значение атрибута модели устройства, задающего стратегию вытеснения, равное \texttt{none}, означает, что при неуспешном обращении в это устройство замещение не производится. Здесь и далее символами $t_1, t_2, ..., t_m$ обозначаются аргументы-ключи инициализирующих обращений, $r_1, r_2, ..., r_m$ --- аргументы-регионы инициализирующих обращений, $k_1, k_2, ..., k_n$ --- аргументы-ключи обращений в инструкциях тестового шаблона, $R_1, R_2, ..., R_n$ --- аргументы-регионы обращений в инструкциях тестового шаблона, $S_1, S_2, ..., S_n$ --- успешности обращений в инструкциях тестового шаблона ($S_i = hit$ или $S_i = miss$).

\begin{theorem}[Корректность алгоритма генерации ограничений на ключи обращений для таблицы, стратегия вытеснения которой не \texttt{none}]\label{mirror_correctness}
\CorrectnessMirror
\end{theorem}

\begin{theorem}[Полнота алгоритма генерации ограничений на ключи обращений для таблицы, стратегия вытеснения которой есть \texttt{none}]\label{mirror_fullness_none}
\FullnessMirrorNone
\end{theorem}

Стратегию вытеснения будем называть \emph{существенно вытесняющей}, если $w$ промахов в один регион полностью вытесняют его предыдущее содержимое ($w$ --- значение параметра \texttt{lines} таблицы).

\begin{theorem}[Полнота алгоритма генерации ограничений на ключи обращений для таблицы, стратегия вытеснения которой не \texttt{none} и является \textbf{существенно вытесняющей}]\label{mirror_fullness}
\FullnessMirror
\end{theorem}

В разделе 2.3.2 рассматриваются \emph{таблицы вытеснения}, которые позволяют формализовать стратегии вытеснения. Таблицы вытеснения были предложены в 2008 году исследователями из Университета Саарланда. С использованием таблиц вытеснения в разделе 2.3.3 сформулированы и доказаны теоремы о том, что стратегии вытеснения LRU, FIFO и Pseudo-LRU являются существенно вытесняющими:
\begin{theorem}\label{thm:LRU_essential}
Стратегия вытеснения LRU является существенно вытесняющей.
\end{theorem}

\begin{theorem}
  Стратегия вытеснения FIFO является существенно вытесняющей.
\end{theorem}

\begin{theorem}\label{thm:PseudoLRU_essential} \PseudoLRUEssential \end{theorem}

В этом же разделе исследуется вопрос длины инициализирующей последовательности. Сформулирована и доказана верхняя оценка достаточного количества инициализирующих обращений в устройство подсистемы управления памяти:
\begin{utv}[Верхняя оценка количества инициализирующих обращений]
$$m \leqslant n \cdot (n + 2w)$$ где $w$ --- значение параметра \texttt{lines} таблицы, $n$ --- количество обращений в таблицу в шаблоне.
\end{utv}

Для стратегии вытеснения LRU в этом же разделе сформулирована и доказана более сильная оценка количества инициализирующих обращений:
\begin{theorem}[Верхняя оценка количества инициализирующих обращений для
стратегии вытеснения \LRU]\label{thm_mirror_lenth_lru} \UpperBoundLRUMirror
\end{theorem}

В разделе 2.4 предложено новое определение стратегии вытеснения \PseudoLRU. Обычно при определении \PseudoLRU предлагают рассматривать для региона упорядоченное бинарное дерево с пометками в нелистовых вершинах, листовым вершинам дерева соответствуют строки региона. Как и прежде, обращения осуществляются к одной из листовых вершин дерева, что приводит к изменению пометок вершин пути в неё из корневой вершины. Вытесняемая строка определяется также на основе пометок вершин дерева. Новое определение задает стратегию вытеснения \PseudoLRU как изменение битовых векторов (\emph{\PseudoLRU-ветвей}), сопоставленных строкам региона. Это определение позволит сократить количество ограничений и ускорить их разрешение. Сформулирована и доказана теорема, задающее изменение \PseudoLRU-ветвей и показывающая эквивалентность нового определения \PseudoLRU старому ($W = \log_2 w$, для стратегии вытеснения \PseudoLRU допустимы лишь те $w$, которые являются степенями двойки, \emph{абсолютная позиция}(или просто, \emph{позиция}) --- это номер строки в регионе, \emph{относительная позиция} позиции $i$ относительно позиции $j$ будем назыаать $i \oplus j$ и обозначать как $\pi_j^i$):
\begin{theorem}[Инвариантность преобразования \PseudoLRU-ветвей относительными
позициями]\label{thm_pseudoLRU_invariant} \PseudoLRUInvariant
\end{theorem}

В разделе 2.5 предложен метод построения ограничений для свойства <<быть вытесненным к моменту заданного обращения в таблицу>> --- \emph{метод полезных обращений}. С помощью него это свойство выражается в виде ограничений в операциях над битовыми строками и целочисленной линейной арифметике. В разделе предложена формализация понятия \emph{полезной для вытеснения} (или просто, \emph{полезной}) инструкции. \emph{Формулой полезного обращения} будем называть предикат, истинный для всех обращений, являющихся полезными, и ложный на всех обращениях, не являющихся полезными. В рамках метода полезных обращений свойство <<быть вытесненным>> рассматривается как ограничение снизу количества предыдущих обращений, являющихся полезными.

В разделе 2.5.1 предложено и формально обосновано представление свойства <<быть вытесненным>> для стратегии вытеснения LRU в виде ограничений, составленное по методу полезных обращений (<<||>> --- операция битовой конкатенации, выражение $[\phi]$ равно 1, если $\phi$ истинно, и равно 0 в противном случае):
\begin{theorem}[Выражение свойства <<быть вытесненным>> для \LRU]\label{correct_mirror_LRU} \LRUusefuls
\end{theorem}

В разделе 2.5.2 предложено и формально обосновано представление свойства <<быть вытесненным>> для стратегии вытеснения \FIFO  в виде ограничений, составленное по методу полезных обращений.

В разделе 2.5.3 предложено и формально обосновано представление свойства <<быть вытесненным>> для стратегии вытеснения \PseudoLRU в виде ограничений, составленное по методу полезных обращений:
\begin{theorem}[Выражение свойства <<быть вытесненным>> для \PseudoLRU]\label{correct_mirror_PLRU} \PLRUusefuls

$\pi_i$ --- позиции --- дополнительные переменные, для которых надо построить ограничения:
конъюнкцию для каждой пары $(s_i,\pi_i)$ и $(s_j, \pi_j)$ при $j > i$ ограничений:
\begin{itemize}
    \item если $j$'е обращение успешное, то $(\pi_i||R(s_i) =
\pi_j||R(s_j)~\wedge$ $$\pi_i||R(s_i) \notin \{\pi_{m_1}||R(s_{m_1}),
\pi_{m_2}||R(s_{m_2}), \dots, \pi_{m_n}||R(s_{m_n})\}) \rightarrow s_i = s_j$$
    \item в противном случае $(\pi_i||R(s_i) =
\pi_j||R(s_j)~\wedge$ $$\pi_i||R(s_i) \notin \{\pi_{m_1}||R(s_{m_1}),
\pi_{m_2}||R(s_{m_2}), \dots, \pi_{m_n}||R(s_{m_n})\}) \rightarrow s_i \neq
s_j$$
\end{itemize}
где $(\pi_{m_1},R(s_{m_1})), (\pi_{m_2},R(s_{m_2})), \dots,
(\pi_{m_n},R(s_{m_n}))$ --- позиции и регионы\\неуспешных обращений,
расположенных между $i$'м и $j$'м.
\end{theorem}

В разделе 2.5.4 освещаются некоторые вопросы сложности разрешения ограничений, которые строятся согласно методу полезных обращений.


В разделе 2.6 рассматривается последний этап построения тестовой программы --- этап конструирования текста программы. Текст тестовой программы состоит из инициализирующей части и инструкций тестового шаблона. Инициализирующая часть состоит из инструкций для помещения вычисленных на предыдущем этапе начальных значений в соответствующие регистры и последовательности инструкций, обращающихся в соответствующее устройство подсистемы управления памяти по вычисленным ключам в вычисленные регистры с вычисленными данными. Зачастую конструирование таких инструкций не представляет сложности. Пример противоположного случая --- инициализация многоуровневой кэш-памяти в случае, если инициализацию отдельных уровней кэш-памяти нельзя осуществить отдельно от остальных уровней. Поэтому в разделе 2.6 предложен и метод конструирования последовательности инициализирующих инструкций, учитывающий особенности многоуровневой кэш-памяти.

\paragraph{В третьей главе} дается оценка предлагаемым методам. В разделах 3.1, 3.2 и 3.3 показывается, что подсистемы управления памяти микропроцессоров архитектур MIPS, PowerPC и IA-32 можно представить в виде набора таблиц и формализовать варианты инструкций, оперирующих с памятью. Причем имеется документация по каждой архитектуре, где эти варианты уже описаны на соответствующем псевдокоде. В разделе 3.4 описана автоматизация некоторых этапов предлагаемого во второй главе подхода: генератор ограничений, решатель ограничений и конструктор текстов тестовых программ. Решатель ограничений --- это внешний инструмент (Z3) и разрабатывать его для автоматизации подхода не надо, что сильно сокращает трудоемкость автоматизации подхода. Затронут вопрос переиспользования перечисленных компонентов при смене микропроцессора. Был реализован прототип генератора тестовых программ для архитектуры MIPS64. В разделе 3.5 описаны эксперименты над этим прототипом по оценке времени построения тестовых программ и вероятности завершения построения за 60 секунд. Эксперименты показали увеличение допустимого размера тестовых шаблонов до 9-12 инструкций (по сравнению с 2-3 инструкциями в доступных инструментах). В разделе 3.6 проведено сравнение с инструментом Genesys-Pro (IBM): выделены сходства и отличия, преимущества и недостатки предложенных методов по сравнению с Genesys-Pro. В разделе 3.7 проведено сравнение с работами, проводящимися в Intel.

\paragraph{В Заключении} диссертационной работы перечисляются ее основные результаты.

% ----------------------------------------------------------------

\section*{Основные результаты работы}
\Results


% ----------------------------------------------------------------
\renewcommand\bibsection{\section*{Публикации по теме диссертации}}
%\section*{Публикации по теме диссертации}
\bibliographystyle{gost780s}
\bibliography{../delta/thesis}
% ----------------------------------------------------------------

\end{document}


%%%
%% формулировка результатов
%%% 